Probabilistic Programming with Gaussian Distributions

Probabilistic programming is simply programming with probabilities. More concretely, in probabilistic programming we perform random choices and then ask what the probability of a result. For example consider a program:

Q: What is the probability of x==y? A: 50%.

An essential component of probabilistic programming is how to support these two features for each distribution described by a probabilistic program: A way to take a random sample from the distribution, and a way to estimate the probability density of a certain sample.

Seminar

• Paper:
  • Compositional Semantics for Probabilistic Programs with Exact Conditioning
• Tool:
  • https://github.com/damast93/GaussianInfer

Project

In a project, we will implementing a simple DSL following the strategy described above in the paper about gaussian probabilities with in Lean. Lean is a modern, general-purpose programming language featuring advanced functional programming constructs such as pattern matching, recursion, immutable datastructures, type classes, dependent types and more. At the same time, Lean compiles to C++, featuring easy interopability with low-level libraries where necessary. Let's try it out and see how far we can go :)